TLA+ Tools

Leslie Lamport

Last modified on 10 February 2021

Most users of TLA+ will run the TLA+ tools from the TLA+ Toolbox. How to download them and run them outside the Toolbox is explained here.

The Tools

SANY Syntactic Analyzer [hide]

A parser and syntax checker for TLA+ specifications. It catches parsing errors and some semantic errors such as priming an expression containing primed variables. It was written by Jean-Charles Grégoire, David Jefferson, and Yuan Yu.

TLC Model Checker [hide]

A model checker and simulator for executable TLA+ specifications, which include most specifications written by engineers. It is an explicit-state model checker that can check both safety and liveness properties. For safety checking, TLC achieves an approximately linear speedup on modern large computers using 32 or more cores. It can further speed-up model checking by running on a network of computers, and provides easy deployment on cloud systems. TLC was written by Yuan Yu and extended by Markus Kuppe.

PlusCal Translator [hide]

A translator from the PlusCal algorithm language to TLA+. It was written by Keith Marzullo and the author of this web page.

TLAPS Proof System [hide]

A system for mechanically checking proofs written in TLA+, including proofs of the kinds of properties described here. It is being developed at the Microsoft Research–Inria Joint Centre. See the TLAPS home page for more information. The first version of TLAPS was written by Kaustuv Chaudhuri. Improvements have been made by Damien Doligez, Stephan Merz, Hernán Vanzetto, Tomer Libal, Martin Riener, and Denis Cousineau.

TLATeX Pretty-Printer [hide]

A program for typesetting TLA+ specifications. It is used by the Toolbox's Produce PDF Version command to generate and display a pdf file with a pretty-printed version of a specification. Chapter 13 of Specifying Systems has some tips on formatting this version. TLATeX can also be used outside the Toolbox to include TLA+ formulas and PlusCal code as part of a LaTeX document. Click here to find out how to run TLATeX outside the Toolbox. Here are instructions for how to include TLA+ formulas and PlusCal code in a LaTeX document. You will have to download the tlatex.sty package file to use TLATeX with LaTeX.

Documentation

Except for the PlusCal translator and TLAPS, the tools are described in the book Specifying Systems. Documentation of the PlusCal translator can be found here. Some documentation of the TLAPS proof system can be found on its web site and in the TLA+ Hyperbook.

The current versions of the language and tools differ somewhat from the ones described in the book. Most notably, language constructs for writing proofs have been added to TLA+, and a number of features have been added to TLC. All significant changes to the tools since the book was written are described in the document Current Versions of the TLA+ Tools, which contains a complete list of TLC command-line options. Changes to the language are described in this web page.

Known bugs in the tools are reported on the TLA+ Github issues page. Requests for additional features are also posted there. Tell us about any problems or inadequacies you find with the tools. But please remember that we are a small number of people trying to respond to the needs of an ever-growing number of users.